home *** CD-ROM | disk | FTP | other *** search
/ ASME's Mechanical Engine…ing Toolkit 1997 December / ASME's Mechanical Engineering Toolkit 1997 December.iso / ai / prlg195b.lzh / LOGIC.LZH / WANG.PRO < prev   
Text File  |  1987-04-03  |  3KB  |  96 lines
  1. /* Notes from Bob: 
  2.  
  3. To run this program on versions FS and higher, remove the
  4. built-in definition of member, and "hidelog" "&", or change
  5. "&" to another symbol.
  6.  
  7. After loading, give the goal of "start.<CR>"
  8.  
  9. The printout I got from the author indicates that the following
  10. would be a valid test, to be entered after the prompt "Write
  11. an argument:"
  12.  
  13.      (~p & r) => ((p v q) => (r & q)).
  14.  
  15.  
  16. */
  17.  
  18.  
  19.  
  20.  /*     WANG.PRO, PDPROLOG version, BYTE, oct/86 */
  21. /*      adapted by Xavier Salazar Resines, feb/2/87    */
  22.  
  23.  
  24. /* This works for all the versions: */
  25. ?-hidelog; true.
  26.  
  27. ?-op(240,xfy,'<=>').
  28. ?-op(230,xfy,'=>').
  29. ?-op(220,xfy,'v').
  30. ?-op(210,xfy,'&').
  31. ?-op(200,fy,'~').
  32.  
  33. start:- print('Write an argument: \n'),read(A),nl,
  34.     print('(*) marks the main => position'),nl,
  35.     print('------------------------------'),nl,argument(A).
  36.  
  37. argument(A):- nl, test([] & [] => [] & [A]),!,nl,
  38.             print('Valid argument !'),nl,nl,print('Other: ?-start.'),nl.
  39. argument(_):-nl,print('Invalid argument, sorry.'),nl,nl,
  40.         print('Other: ?-start.'),nl.
  41.  
  42. test(A1):- nl,print('Test ',A1),nl,rule(A1,A2,Txt),!,nl,
  43.         print(A2,' ',Txt),nl,test(A2).
  44.  
  45.  
  46. test(L & [H v I|T] => R):- !,nl,print('Two branches for disjunction (*)'),nl,
  47.                 print('--------------------------------'),nl,
  48.              bnch1_disj,test(L & [H|T] => R),
  49.                          bnch2_disj,test(L & [I|T] => R).
  50.  
  51. test(L => R & [H & I|T]):- !,nl,print('(*) Two branches for conjunction'),nl,
  52.                 print('--------------------------------'),nl, 
  53.             bnch1_conj,test(L => R & [H|T]),
  54.                         bnch2_conj,test(L => R & [I|T]).
  55.  
  56. test(L & [H|T] => R):- !,nl,print('       [] <- [atom] (*)'),
  57.             test([H|L] & T => R).
  58. test(L => R & [H|T]):- !,nl,print('       (*) [] <- [atom]'),
  59.             test(L => [H|R] & T).è
  60. test(A):- tautology(A),nl,print('Tautology.'),!,nl.
  61. test(_):- nl,print('Can not test this step'),fail.
  62.  
  63. rule(L & [H => I|T] => R, L & [~ H v I|T] => R, 'by definition (*)').
  64. rule(L => R & [H => I|T], L => R & [~ H v I|T], '(*) by definition').
  65.  
  66. rule(L & [H <=> I|T] => R, 
  67.    L & [(H => I) & (I => H)|T] => R, 'conditionals by biconditional (*)').
  68. rule(L => R & [H <=> I|T], 
  69.    L => R & [(H => I) & (I => H)|T], '(*) conditionals by biconditional').
  70.  
  71. rule(L & [~ H|T] => R & R2, 
  72.   L & T => R & [H|R2], 'from negated (*) to unnegated').
  73. rule(L1 & L2 => R & [~ H|T], 
  74.   L1 & [H|L2] => R & T, 'to unnegated (*) from negated').
  75.  
  76. rule(L & [H & I|T] => R, L & [H,I|T] => R, 'comma for conjunction (*)').
  77.  
  78. rule(L => R & [H v I|T], L => R & [H,I|T], '(*) comma for disjunction').
  79.  
  80. tautology(L & [] => R & []):- members(M,L),members(M,R).
  81.  
  82. bnch1_disj:- nl,print('Branch 1 disjunction').
  83. bnch2_disj:- nl,print('Branch 2 disjunction').
  84.  
  85. bnch1_conj:- nl,print('Branch 1 conjunction').
  86. bnch2_conj:- nl,print('Branch 2 conjunction').
  87.  
  88. members(H,[H|_]).
  89. members(I,[_|T]):- members(I,T).
  90.  
  91. ?- cls,nl,nl,nl,print('Write: ?-start.<RET>'),nl,
  92. print('After do write the argument, BINARY expressions within parentheses'),
  93. nl,nl. 
  94.  
  95.  
  96.